Search Results

Documents authored by Katoen, Joost-Pieter


Document
Scalable Analysis of Probabilistic Models and Programs (Dagstuhl Seminar 23241)

Authors: Sebastian Junges, Joost-Pieter Katoen, Scott Sanner, Guy Van den Broeck, and Bahare Salmani

Published in: Dagstuhl Reports, Volume 13, Issue 6 (2024)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 23241 "Scalable Analysis of Probabilistic Models and Programs". The seminar brought together researchers from probabilistic graphical models, verification of probabilistic programming languages, and probabilistic planning. The communities bring vastly different perspectives on the methods and goals of inference under uncertainty. In this seminar, we worked towards a common understanding of how the different angles yield subtle differences in the problem statements and how the different methods provide different strengths and weaknesses. The report describes the different areas, the activities during the seminar including hot topics that were vividly discussed, and an overview of the technical talks.

Cite as

Sebastian Junges, Joost-Pieter Katoen, Scott Sanner, Guy Van den Broeck, and Bahare Salmani. Scalable Analysis of Probabilistic Models and Programs (Dagstuhl Seminar 23241). In Dagstuhl Reports, Volume 13, Issue 6, pp. 1-21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@Article{junges_et_al:DagRep.13.6.1,
  author =	{Junges, Sebastian and Katoen, Joost-Pieter and Sanner, Scott and Van den Broeck, Guy and Salmani, Bahare},
  title =	{{Scalable Analysis of Probabilistic Models and Programs (Dagstuhl Seminar 23241)}},
  pages =	{1--21},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{13},
  number =	{6},
  editor =	{Junges, Sebastian and Katoen, Joost-Pieter and Sanner, Scott and Van den Broeck, Guy and Salmani, Bahare},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.13.6.1},
  URN =		{urn:nbn:de:0030-drops-196362},
  doi =		{10.4230/DagRep.13.6.1},
  annote =	{Keywords: model counting, probabilistic inference, probabilistic model checking, probabilistic planning, probabilistic programs}
}
Document
Towards Concurrent Quantitative Separation Logic

Authors: Ira Fesefeldt, Joost-Pieter Katoen, and Thomas Noll

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)


Abstract
In this paper, we develop a novel verification technique to reason about programs featuring concurrency, pointers and randomization. While the integration of concurrency and pointers is well studied, little is known about the combination of all three paradigms. To close this gap, we combine two kinds of separation logic - Quantitative Separation Logic and Concurrent Separation Logic - into a new separation logic that enables reasoning about lower bounds of the probability to realise a postcondition by executing such a program.

Cite as

Ira Fesefeldt, Joost-Pieter Katoen, and Thomas Noll. Towards Concurrent Quantitative Separation Logic. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 25:1-25:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{fesefeldt_et_al:LIPIcs.CONCUR.2022.25,
  author =	{Fesefeldt, Ira and Katoen, Joost-Pieter and Noll, Thomas},
  title =	{{Towards Concurrent Quantitative Separation Logic}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{25:1--25:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.25},
  URN =		{urn:nbn:de:0030-drops-170881},
  doi =		{10.4230/LIPIcs.CONCUR.2022.25},
  annote =	{Keywords: Randomization, Pointers, Heap-Manipulating, Separation Logic, Concurrency}
}
Document
Complete Volume
LIPIcs, Volume 138, MFCS'19, Complete Volume

Authors: Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)


Abstract
LIPIcs, Volume 138, MFCS'19, Complete Volume

Cite as

44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@Proceedings{rossmanith_et_al:LIPIcs.MFCS.2019,
  title =	{{LIPIcs, Volume 138, MFCS'19, Complete Volume}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019},
  URN =		{urn:nbn:de:0030-drops-112092},
  doi =		{10.4230/LIPIcs.MFCS.2019},
  annote =	{Keywords: Theory of computation}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)


Abstract
Front Matter, Table of Contents, Preface, Conference Organization

Cite as

44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{rossmanith_et_al:LIPIcs.MFCS.2019.0,
  author =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{0:i--0:xvi},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.0},
  URN =		{urn:nbn:de:0030-drops-109444},
  doi =		{10.4230/LIPIcs.MFCS.2019.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
On the Complexity of Reachability in Parametric Markov Decision Processes

Authors: Tobias Winkler, Sebastian Junges, Guillermo A. Pérez, and Joost-Pieter Katoen

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
This paper studies parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where transitions probabilities are described by polynomials over a finite set of parameters. Fixing values for all parameters yields MDPs. In particular, this paper studies the complexity of finding values for these parameters such that the induced MDP satisfies some reachability constraints. We discuss different variants depending on the comparison operator in the constraints and the domain of the parameter values. We improve all known lower bounds for this problem, and notably provide ETR-completeness results for distinct variants of this problem. Furthermore, we provide insights in the functions describing the induced reachability probabilities, and how pMDPs generalise concurrent stochastic reachability games.

Cite as

Tobias Winkler, Sebastian Junges, Guillermo A. Pérez, and Joost-Pieter Katoen. On the Complexity of Reachability in Parametric Markov Decision Processes. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{winkler_et_al:LIPIcs.CONCUR.2019.14,
  author =	{Winkler, Tobias and Junges, Sebastian and P\'{e}rez, Guillermo A. and Katoen, Joost-Pieter},
  title =	{{On the Complexity of Reachability in Parametric Markov Decision Processes}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{14:1--14:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.14},
  URN =		{urn:nbn:de:0030-drops-109162},
  doi =		{10.4230/LIPIcs.CONCUR.2019.14},
  annote =	{Keywords: Parametric Markov decision processes, Formal verification, ETR, Complexity}
}
Document
Machine Learning and Model Checking Join Forces (Dagstuhl Seminar 18121)

Authors: Nils Jansen, Joost-Pieter Katoen, Pusmeet Kohli, and Jan Kretinsky

Published in: Dagstuhl Reports, Volume 8, Issue 3 (2018)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 18121 "Machine Learning and Model Checking Join Forces". This Dagstuhl Seminar brought together researchers working in the fields of machine learning and model checking. It helped to identify new research topics on the one hand and to help with current problems on the other hand.

Cite as

Nils Jansen, Joost-Pieter Katoen, Pusmeet Kohli, and Jan Kretinsky. Machine Learning and Model Checking Join Forces (Dagstuhl Seminar 18121). In Dagstuhl Reports, Volume 8, Issue 3, pp. 74-93, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@Article{jansen_et_al:DagRep.8.3.74,
  author =	{Jansen, Nils and Katoen, Joost-Pieter and Kohli, Pusmeet and Kretinsky, Jan},
  title =	{{Machine Learning and Model Checking Join Forces (Dagstuhl Seminar 18121)}},
  pages =	{74--93},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{8},
  number =	{3},
  editor =	{Jansen, Nils and Katoen, Joost-Pieter and Kohli, Pusmeet and Kretinsky, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.8.3.74},
  URN =		{urn:nbn:de:0030-drops-92988},
  doi =		{10.4230/DagRep.8.3.74},
  annote =	{Keywords: artificial intelligence, cyber-physical systems, formal methods, formal verification, logics, machine learning, model checking, quantitative verification, safety-critical systems}
}
Document
Challenges and Trends in Probabilistic Programming (Dagstuhl Seminar 15181)

Authors: Gilles Barthe, Andrew D. Gordon, Joost-Pieter Katoen, and Annabelle McIver

Published in: Dagstuhl Reports, Volume 5, Issue 4 (2015)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 15181 "Challenges and Trends in Probabilistic Programming". Probabilistic programming is at the heart of machine learning for describing distribution functions; Bayesian inference is pivotal in their analysis. Probabilistic programs are used in security for describing both cryptographic constructions (such as randomised encryption) and security experiments. In addition, probabilistic models are an active research topic in quantitative information now. Quantum programs are inherently probabilistic due to the random outcomes of quantum measurements. Finally, there is a rapidly growing interest in program analysis of probabilistic programs, whether it be using model checking, theorem proving, static analysis, or similar. Dagstuhl Seminar 15181 brought researchers from these various research communities together so as to exploit synergies and realize cross-fertilisation.

Cite as

Gilles Barthe, Andrew D. Gordon, Joost-Pieter Katoen, and Annabelle McIver. Challenges and Trends in Probabilistic Programming (Dagstuhl Seminar 15181). In Dagstuhl Reports, Volume 5, Issue 4, pp. 123-141, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@Article{barthe_et_al:DagRep.5.4.123,
  author =	{Barthe, Gilles and Gordon, Andrew D. and Katoen, Joost-Pieter and McIver, Annabelle},
  title =	{{Challenges and Trends in Probabilistic Programming (Dagstuhl Seminar 15181)}},
  pages =	{123--141},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{5},
  number =	{4},
  editor =	{Barthe, Gilles and Gordon, Andrew D. and Katoen, Joost-Pieter and McIver, Annabelle},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.5.4.123},
  URN =		{urn:nbn:de:0030-drops-53536},
  doi =		{10.4230/DagRep.5.4.123},
  annote =	{Keywords: Bayesian networks, differential privacy, machine learning, probabilistic programs, security, semantics, static analysis, verification}
}
Document
Correct and Efficient Accelerator Programming (Dagstuhl Seminar 13142)

Authors: Albert Cohen, Alastair F. Donaldson, Marieke Huisman, and Joost-Pieter Katoen

Published in: Dagstuhl Reports, Volume 3, Issue 4 (2013)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 13142 "Correct and Efficient Accelerator Programming". The aim of this Dagstuhl seminar was to bring together researchers from various sub-disciplines of computer science to brainstorm and discuss the theoretical foundations, design and implementation of techniques and tools for correct and efficient accelerator programming.

Cite as

Albert Cohen, Alastair F. Donaldson, Marieke Huisman, and Joost-Pieter Katoen. Correct and Efficient Accelerator Programming (Dagstuhl Seminar 13142). In Dagstuhl Reports, Volume 3, Issue 4, pp. 17-33, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


Copy BibTex To Clipboard

@Article{cohen_et_al:DagRep.3.4.17,
  author =	{Cohen, Albert and Donaldson, Alastair F. and Huisman, Marieke and Katoen, Joost-Pieter},
  title =	{{Correct and Efficient Accelerator Programming (Dagstuhl Seminar 13142)}},
  pages =	{17--33},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{3},
  number =	{4},
  editor =	{Cohen, Albert and Donaldson, Alastair F. and Huisman, Marieke and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.3.4.17},
  URN =		{urn:nbn:de:0030-drops-40758},
  doi =		{10.4230/DagRep.3.4.17},
  annote =	{Keywords: Accelerator programming, GPUs, Concurrency, Formal verification, Compilers, Memory models, Architecture, Parallel programming models}
}
Document
Deciding Probabilistic Simulation between Probabilistic Pushdown Automata and Finite-State Systems

Authors: Hongfei Fu and Joost-Pieter Katoen

Published in: LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)


Abstract
This paper studies the decidability and computational complexity of checking probabilistic simulation pre-order between probabilistic pushdown automata (pPDA) and (probabilistic)finite-state systems. We show that checking classical and combined probabilistic similarity are EXPTIME-complete in both directions and become polynomial if both the number of control states of the pPDA and the size of the finite-state system are fixed. These results show that checking probabilistic similarity is as hard as checking similarity in the standard, i.e., non-probabilistic setting.

Cite as

Hongfei Fu and Joost-Pieter Katoen. Deciding Probabilistic Simulation between Probabilistic Pushdown Automata and Finite-State Systems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 445-456, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{fu_et_al:LIPIcs.FSTTCS.2011.445,
  author =	{Fu, Hongfei and Katoen, Joost-Pieter},
  title =	{{Deciding Probabilistic Simulation between Probabilistic Pushdown Automata and Finite-State Systems}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{445--456},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.445},
  URN =		{urn:nbn:de:0030-drops-33435},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.445},
  annote =	{Keywords: infinite-state systems, probabilistic simulation, probabilistic pushdown automata}
}
Document
07101 Abstracts Collection – Quantitative Aspects of Embedded Systems

Authors: Boudewijn Haverkort, Joost-Pieter Katoen, and Lothar Thiele

Published in: Dagstuhl Seminar Proceedings, Volume 7101, Quantitative Aspects of Embedded Systems (2007)


Abstract
From March 5 to March 9, 2007, the Dagstuhl Seminar 07101 ``Quantitative Aspects of Embedded Systems'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

Cite as

Boudewijn Haverkort, Joost-Pieter Katoen, and Lothar Thiele. 07101 Abstracts Collection – Quantitative Aspects of Embedded Systems. In Quantitative Aspects of Embedded Systems. Dagstuhl Seminar Proceedings, Volume 7101, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{haverkort_et_al:DagSemProc.07101.1,
  author =	{Haverkort, Boudewijn and Katoen, Joost-Pieter and Thiele, Lothar},
  title =	{{07101 Abstracts Collection – Quantitative Aspects of Embedded Systems}},
  booktitle =	{Quantitative Aspects of Embedded Systems},
  pages =	{1--16},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7101},
  editor =	{Boudewijn Haverkort and Joost-Pieter Katoen and Lothar Thiele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07101.1},
  URN =		{urn:nbn:de:0030-drops-11402},
  doi =		{10.4230/DagSemProc.07101.1},
  annote =	{Keywords: Embedded systems, quantitative analysis, model checking, real-time calculus, validation, verification, model-based and model-driven design}
}
Document
07101 Executive Summary – Quantitative Aspects of Embedded Systems

Authors: Boudewijn Haverkort, Joost-Pieter Katoen, and Lothar Thiele

Published in: Dagstuhl Seminar Proceedings, Volume 7101, Quantitative Aspects of Embedded Systems (2007)


Abstract
This is an executive summary of Dagstuhl seminar 07101, March 5--9, 2007.

Cite as

Boudewijn Haverkort, Joost-Pieter Katoen, and Lothar Thiele. 07101 Executive Summary – Quantitative Aspects of Embedded Systems. In Quantitative Aspects of Embedded Systems. Dagstuhl Seminar Proceedings, Volume 7101, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{haverkort_et_al:DagSemProc.07101.2,
  author =	{Haverkort, Boudewijn and Katoen, Joost-Pieter and Thiele, Lothar},
  title =	{{07101 Executive Summary – Quantitative Aspects of Embedded Systems}},
  booktitle =	{Quantitative Aspects of Embedded Systems},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7101},
  editor =	{Boudewijn Haverkort and Joost-Pieter Katoen and Lothar Thiele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07101.2},
  URN =		{urn:nbn:de:0030-drops-11378},
  doi =		{10.4230/DagSemProc.07101.2},
  annote =	{Keywords: Embedded systems, quantitative analysis, model checking, real-time calculus, validation, verification, model-based and model-driven design. Embedded s}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail